$\forall$$T$,${\it T'}$:Type, $a$:($T$ List), $x$:${\it T'}$, $f$:($T$$\rightarrow$${\it T'}$).
\\[0ex]($x$ $\in$ map($f$; $a$)) $\Leftarrow\!\Rightarrow$ ($\exists$$y$:$T$. (($y$ $\in$ $a$) $\wedge$ ($x$ = $f$($y$))))